$\forall$$a$:Atom2. AtomFree(Atom2;$a$)